Termination w.r.t. Q of the following Term Rewriting System could be disproven:

Q restricted rewrite system:
The TRS R consists of the following rules:

from(X) → cons(X)
length → 0
length → s(length1)
length1 → length

Q is empty.


↳ QTRS
  ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

from(X) → cons(X)
length → 0
length → s(length1)
length1 → length

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

from(X) → cons(X)
length → 0
length → s(length1)
length1 → length

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

from(X) → cons(X)
Used ordering:
Polynomial interpretation [25]:

POL(0) = 0   
POL(cons(x1)) = 2·x1   
POL(from(x1)) = 1 + 2·x1   
POL(length) = 0   
POL(length1) = 0   
POL(s(x1)) = 2·x1   




↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

length → 0
length → s(length1)
length1 → length

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

length → 0
length → s(length1)
length1 → length

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

length → 0
Used ordering:
Polynomial interpretation [25]:

POL(0) = 0   
POL(length) = 1   
POL(length1) = 1   
POL(s(x1)) = x1   




↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

length → s(length1)
length1 → length

Q is empty.

The TRS is overlay and locally confluent. By [19] we can switch to innermost.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ Overlay + Local Confluence
            ↳ QTRS
              ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

length → s(length1)
length1 → length

The set Q consists of the following terms:

length
length1


Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

LENGTH1 → LENGTH
LENGTH → LENGTH1

The TRS R consists of the following rules:

length → s(length1)
length1 → length

The set Q consists of the following terms:

length
length1

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ Overlay + Local Confluence
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ UsableRulesProof
                  ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

LENGTH1 → LENGTH
LENGTH → LENGTH1

The TRS R consists of the following rules:

length → s(length1)
length1 → length

The set Q consists of the following terms:

length
length1

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ Overlay + Local Confluence
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ UsableRulesProof
                    ↳ QDP
                      ↳ QReductionProof
                  ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

LENGTH1 → LENGTH
LENGTH → LENGTH1

R is empty.
The set Q consists of the following terms:

length
length1

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

length
length1



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ Overlay + Local Confluence
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ UsableRulesProof
                    ↳ QDP
                      ↳ QReductionProof
                        ↳ QDP
                          ↳ NonTerminationProof
                  ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

LENGTH1 → LENGTH
LENGTH → LENGTH1

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

LENGTH1 → LENGTH
LENGTH → LENGTH1

The TRS R consists of the following rules:none


s = LENGTH evaluates to t =LENGTH

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

LENGTH → LENGTH1
with rule LENGTH → LENGTH1 at position [] and matcher [ ]

LENGTH1 → LENGTH
with rule LENGTH1 → LENGTH

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.




As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ Overlay + Local Confluence
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ UsableRulesProof
                  ↳ UsableRulesProof
                    ↳ QDP
                      ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

LENGTH1 → LENGTH
LENGTH → LENGTH1

R is empty.
The set Q consists of the following terms:

length
length1

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

length
length1



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ Overlay + Local Confluence
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ UsableRulesProof
                  ↳ UsableRulesProof
                    ↳ QDP
                      ↳ QReductionProof
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LENGTH1 → LENGTH
LENGTH → LENGTH1

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.